YES 0.658 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ CR

mainModule FiniteMap
  ((maxFM :: FiniteMap Int a  ->  Maybe Int) :: FiniteMap Int a  ->  Maybe Int)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a


  maxFM :: Ord a => FiniteMap a b  ->  Maybe a
maxFM EmptyFM Nothing
maxFM (Branch key _ _ _ fm_r
case maxFM fm_r of
  Nothing-> Just key
  Just key1-> Just key1


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Case Reductions:
The following Case expression
case maxFM fm_r of
 Nothing → Just key
 Just key1 → Just key1

is transformed to
maxFM0 key Nothing = Just key
maxFM0 key (Just key1) = Just key1



↳ HASKELL
  ↳ CR
HASKELL
      ↳ BR

mainModule FiniteMap
  ((maxFM :: FiniteMap Int a  ->  Maybe Int) :: FiniteMap Int a  ->  Maybe Int)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b


  maxFM :: Ord b => FiniteMap b a  ->  Maybe b
maxFM EmptyFM Nothing
maxFM (Branch key _ _ _ fm_rmaxFM0 key (maxFM fm_r)

  
maxFM0 key Nothing Just key
maxFM0 key (Just key1Just key1


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule FiniteMap
  ((maxFM :: FiniteMap Int a  ->  Maybe Int) :: FiniteMap Int a  ->  Maybe Int)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b


  maxFM :: Ord b => FiniteMap b a  ->  Maybe b
maxFM EmptyFM Nothing
maxFM (Branch key vw vx vy fm_rmaxFM0 key (maxFM fm_r)

  
maxFM0 key Nothing Just key
maxFM0 key (Just key1Just key1


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule FiniteMap
  (maxFM :: FiniteMap Int a  ->  Maybe Int)

module FiniteMap where
  import qualified Maybe
import qualified Prelude

  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b


  maxFM :: Ord b => FiniteMap b a  ->  Maybe b
maxFM EmptyFM Nothing
maxFM (Branch key vw vx vy fm_rmaxFM0 key (maxFM fm_r)

  
maxFM0 key Nothing Just key
maxFM0 key (Just key1Just key1


module Maybe where
  import qualified FiniteMap
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ CR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
QDP
                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_maxFM(Branch(wv30, wv31, wv32, wv33, wv34), h) → new_maxFM(wv34, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: